'''
Created on 21/09/2009

@author: b1u3fox
'''

class Proposicion(object):
    pass


class Enunciado(Proposicion):
    def __init__(self, id=None, descripcion=None):
        self.id = id
        self.descripcion = descripcion
        
    def __repr__(self):
        return self.id
    

class ProposicionMolecular(Proposicion):
    def __init__(self, proposicion1, proposicion2=None):
        self.proposicion1 = proposicion1
        self.proposicion2 = proposicion2
        
    def __eq__(self, otro):
        return (self.__class__ == otro.__class__ and
                self.proposicion1 == otro.proposicion1 and
                self.proposicion2 == otro.proposicion2)
        
    def __ne__(self, otro):
        return (self.__class__ != otro.__class__ or
                self.proposicion1 != otro.proposicion1 or
                self.proposicion2 != otro.proposicion2) 


class Negacion(ProposicionMolecular):
    def __init__(self, proposicion1):
        ProposicionMolecular.__init__(self, proposicion1)
        
    def __repr__(self):
        return '~' + self.proposicion1.__repr__()
        
    def __eq__(self, otro):
        return (self.__class__ == otro.__class__ and
                self.proposicion1 == otro.proposicion1)
        
    def __ne__(self, otro):
        return (self.__class__ != otro.__class__ or
                self.proposicion1 != otro.proposicion1)


class Disyuncion(ProposicionMolecular):
    def __repr__(self):
        return '(%s | %s)' % (self.proposicion1.__repr__(), 
                              self.proposicion2.__repr__())


class Conjuncion(ProposicionMolecular):
    def __repr__(self):
        return '(%s & %s)' % (self.proposicion1.__repr__(), 
                              self.proposicion2.__repr__())


class Implicacion(ProposicionMolecular):
    def __repr__(self):
        return '(%s -> %s)' % (self.proposicion1.__repr__(), 
                              self.proposicion2.__repr__())


class DobleImplicacion(ProposicionMolecular):
    def __repr__(self):
        return '(%s <-> %s)' % (self.proposicion1.__repr__(), 
                              self.proposicion2.__repr__())


class Objeto(object):
    def __init__(self, id, descripcion=None):
        self.id = id
        self.descripcion = descripcion
        
    def __repr__(self):
        return self.id
    

class Predicado(object):
    def __init__(self, id, cant_variables, descripcion=None):
        self.id = id
        self.cant_variables = cant_variables
        self.descripcion = descripcion
        
    def __repr__(self):
        return self.id
    
    
class Formula(object):
    def __init__(self, variables):
        if not variables:
            msg = 'Debe especificar al menos una variable.'
            raise Exception(msg)
        else:
            self.variables = variables
            
            
class FormulaAtomica(Formula):
    def __init__(self, predicado, variables):
        if predicado.cant_variables != len(variables):
            msg = 'Cantidad de variables incorrecta.'
            raise Exception(msg)
        Formula.__init__(self, variables)
        self.predicado = predicado
        
    def __repr__(self):
        return str(self.predicado) + ('[%s]' % ', '.join(self.variables))
    
    
class FormulaMolecular(Formula):
    def __init__(self, formula1, formula2=None):
        variables = formula1.variables
        if formula2:
            variables = list(set(variables + formula2.variables))
        Formula.__init__(self, variables)
        self.formula1 = formula1
        self.formula2 = formula2
        
    def __eq__(self, otra):
        return (self.__class__ == otra.__class__ and
                self.formula1 == otra.formula1 and
                self.formula2 == otra.formula2)
        
    def __ne__(self, otra):
        return (self.__class__ != otra.__class__ or
                self.formula1 != otra.formula1 or
                self.formula2 != otra.formula2)
        
        
class FNegacion(FormulaMolecular):
    def __init__(self, formula1):
        Formula.__init__(self, formula1)
        
    def __repr__(self):
        return '~' + self.formula1.__repr__()
        
    def __eq__(self, otra):
        return (self.__class__ == otra.__class__ and
                self.formula1 == otra.formula1)
        
    def __ne__(self, otra):
        return (self.__class__ != otra.__class__ or
                self.formula1 != otra.formula1)


class FDisyuncion(FormulaMolecular):
    def __repr__(self):
        return '(%s | %s)' % (self.formula1.__repr__(), 
                              self.formula2.__repr__())


class FConjuncion(FormulaMolecular):
    def __repr__(self):
        return '(%s & %s)' % (self.formula1.__repr__(), 
                              self.formula2.__repr__())


class FImplicacion(FormulaMolecular):
    def __repr__(self):
        return '(%s -> %s)' % (self.formula1.__repr__(), 
                              self.formula2.__repr__())


class FDobleImplicacion(FormulaMolecular):
    def __repr__(self):
        return '(%s <-> %s)' % (self.formula1.__repr__(), 
                              self.formula2.__repr__())
    
    
class Cuantificador(object):
    EXISTENCIAL = 1
    UNIVERSAL = 2
    
    def __init__(self, tipo):
        self.tipo = tipo
        
    def __repr__(self):
        if self.tipo == self.EXISTENCIAL:
            return '%'
        if self.tipo == self.UNIVERSAL:
            return '@'
        return 'CUANTIFICADOR DESCONOCIDO'


class ProposicionPredicativa(Proposicion):
    def __init__(self, formula, elementos):
        self.formula = formula
        if elementos:
            for variable in formula.variables:
                if not elementos.has_key(variable):
                    msg = 'Las variables y los elementos no coinciden.'
                    raise Exception
                elif elementos[variable] == None:
                    msg = 'Elemento nulo para la variable %s' % variable
                    raise Exception
            self.elementos = elementos
        elif formula:
            self.elementos = {}
            for v in self.formula.variables:
                self.elementos[v] = None
        
    def __repr__(self):
        repr = ''
        variables = self.formula.variables
        variables.sort()
        for variable in variables:
            if isinstance(self.elementos[variable], Cuantificador):
                cuantificador = self.elementos[variable]
                if cuantificador.tipo == Cuantificador.EXISTENCIAL:
                    separador = ':'
                else:
                    separador = ','
                repr += '%s%s%s ' % (str(cuantificador), variable, separador)
        formula_str = str(self.formula)
        for variable in self.formula.variables:
            elemento = self.elementos[variable]
            if isinstance(elemento, Objeto):
                formula_str = formula_str.replace(variable, elemento.__repr__())
        repr += formula_str
        return repr